<html>
<head><meta charset="utf-8"><title>coinduction in the recursive solver chalk#399 · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html">coinduction in the recursive solver chalk#399</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="195762762"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/195762762" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#195762762">(Apr 29 2020 at 20:03)</a>:</h4>
<p>Hey <span class="user-mention" data-user-id="283967">@Zahari Dichev</span> --</p>



<a name="195762777"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/195762777" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#195762777">(Apr 29 2020 at 20:03)</a>:</h4>
<p>let's move further discussion to this topic</p>



<a name="195762797"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/195762797" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#195762797">(Apr 29 2020 at 20:03)</a>:</h4>
<p>Also <span class="user-mention" data-user-id="129457">@Florian Diebold</span> is the one who did most of the impl work on the recursive solver</p>



<a name="195762856"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/195762856" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#195762856">(Apr 29 2020 at 20:04)</a>:</h4>
<p>I've not put a lot of thought either into how to map the coinduction work we did on the SLG solver to the recursive one, but <em>should</em> map over <em>fairly</em> analogously --</p>



<a name="195763176"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/195763176" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#195763176">(Apr 29 2020 at 20:06)</a>:</h4>
<p>the details of the docs don't match, but e.g. the idea of a "strand", in the recursive solver, is basically just "the program stack"</p>



<a name="195763208"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/195763208" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#195763208">(Apr 29 2020 at 20:06)</a>:</h4>
<p>anyway, have to run for now</p>



<a name="196894798"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/196894798" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#196894798">(May 08 2020 at 13:25)</a>:</h4>
<p>Sorry this has taken a bit more time. I have had some other unrelated issues that needed dealing with. Will continue to dig in.<br>
On another note the this video: <a href="https://www.youtube.com/watch?v=Ny2928cGDoM&amp;t=3003s" title="https://www.youtube.com/watch?v=Ny2928cGDoM&amp;t=3003s">https://www.youtube.com/watch?v=Ny2928cGDoM&amp;t=3003s</a> plus the related ones  are quite useful for understanding the general concepts: <a href="https://www.youtube.com/watch?v=Ny2928cGDoM&amp;t=3003s" title="https://www.youtube.com/watch?v=Ny2928cGDoM&amp;t=3003s">https://www.youtube.com/watch?v=Ny2928cGDoM&amp;t=3003s</a>. Should we add them to the chalk book?</p>
<div class="youtube-video message_inline_image"><a data-id="Ny2928cGDoM" href="https://www.youtube.com/watch?v=Ny2928cGDoM&amp;t=3003s" title="https://www.youtube.com/watch?v=Ny2928cGDoM&amp;t=3003s"><img src="https://i.ytimg.com/vi/Ny2928cGDoM/default.jpg"></a></div>



<a name="196894908"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/196894908" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#196894908">(May 08 2020 at 13:26)</a>:</h4>
<p>Also has another question. I read the docs on the recursive solver but I fail to understand what is the general plan here. Just have the two solvers working side by side and gradually evaluate which one is a better fit and transition to it completely?</p>



<a name="196897004"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/196897004" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#196897004">(May 08 2020 at 13:45)</a>:</h4>
<p>We are still evaluating, but I am expecting to consolidate on one solver eventually.</p>



<a name="196897883"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/196897883" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#196897883">(May 08 2020 at 13:54)</a>:</h4>
<p>I see, makes sense. What are the evaluation criteria. I guess what I am asking is, what are the things that are compared and shall eventually inform the consolidation solution ?</p>



<a name="196898973"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/196898973" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#196898973">(May 08 2020 at 14:03)</a>:</h4>
<p>We haven't enumerated specific criteria, but some of the considerations might be</p>
<h1>Pro recursive solver</h1>
<ul>
<li>we see a path (not yet realized) for integrating into salsa and query systems</li>
<li>it can handle assoc type ambiguity</li>
<li>it has a clearer parallelization path</li>
</ul>
<h1>Pro SLG</h1>
<ul>
<li>it is more complete</li>
</ul>



<a name="196898999"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/196898999" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#196898999">(May 08 2020 at 14:03)</a>:</h4>
<p>another criteria would be runtime performance, when we get around to testing that</p>



<a name="197605815"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197605815" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197605815">(May 14 2020 at 19:26)</a>:</h4>
<p>After a bit of hardship trying to understand how all of it. fits together, I have a branch that tries to tackle this issue. The tests that were not passing before pass now. Just need to do some sanity checking and will post a PR tomorrow.</p>



<a name="197605892"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197605892" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197605892">(May 14 2020 at 19:27)</a>:</h4>
<p>Tried to use the concept of <code>delayed goals</code> described in the initial notes that elaborate on the problem. Just need to check a few more things</p>



<a name="197689262"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197689262" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197689262">(May 15 2020 at 13:22)</a>:</h4>
<p>Alright. So here is the PR: <a href="https://github.com/rust-lang/chalk/pull/457">https://github.com/rust-lang/chalk/pull/457</a></p>



<a name="197726980"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197726980" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197726980">(May 15 2020 at 17:43)</a>:</h4>
<p>That being said, i am keen to pick up some more stuff.  If there any future plans for the recursive solver or performance, etc that will be great</p>



<a name="197727015"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197727015" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197727015">(May 15 2020 at 17:43)</a>:</h4>
<p>Infact i find the codebase incredibly interesting :)</p>



<a name="197735660"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197735660" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197735660">(May 15 2020 at 18:48)</a>:</h4>
<p><span class="user-mention" data-user-id="283967">@Zahari Dichev</span> Since you've looked around the recursive solver (and presumably chalk-engine for some coinduction code) the first bullet point here might be good: <a href="https://github.com/rust-lang/chalk/issues/456">https://github.com/rust-lang/chalk/issues/456</a></p>



<a name="197735781"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197735781" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197735781">(May 15 2020 at 18:49)</a>:</h4>
<p>Got it</p>



<a name="197735805"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197735805" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197735805">(May 15 2020 at 18:49)</a>:</h4>
<p>the other to points are actually pretty easy</p>



<a name="197735953"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197735953" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197735953">(May 15 2020 at 18:50)</a>:</h4>
<p>Might try to tackle them as well</p>



<a name="197735985"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197735985" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197735985">(May 15 2020 at 18:51)</a>:</h4>
<p>What about the overall direction of the recirsive solver</p>



<a name="197736017"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197736017" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197736017">(May 15 2020 at 18:51)</a>:</h4>
<p>Are there any other pieces of work that are about to be addressed ?</p>



<a name="197736036"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197736036" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197736036">(May 15 2020 at 18:51)</a>:</h4>
<p>I mean what is the general plan for it ?</p>



<a name="197736253"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197736253" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197736253">(May 15 2020 at 18:53)</a>:</h4>
<p>Hmm, not exactly sure.</p>



<a name="197736309"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197736309" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197736309">(May 15 2020 at 18:53)</a>:</h4>
<p>I don't know if there's anything <em>right now</em> that we know needs to be done with the recursive solver specifically</p>



<a name="197736421"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197736421" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197736421">(May 15 2020 at 18:54)</a>:</h4>
<p>long term though, we need to/will decide whether to stick with the recursive solver or to use SLG</p>



<a name="197736454"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197736454" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197736454">(May 15 2020 at 18:54)</a>:</h4>
<p>But I think to make those decisions, we really need more data</p>



<a name="197736557"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197736557" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197736557">(May 15 2020 at 18:55)</a>:</h4>
<p>As <span class="user-mention" data-user-id="116009">@nikomatsakis</span> mentioned above, there are some considerations for both</p>



<a name="197973037"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197973037" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197973037">(May 18 2020 at 17:57)</a>:</h4>
<p>(I'm reading the PR now)</p>



<a name="197991843"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197991843" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197991843">(May 18 2020 at 20:32)</a>:</h4>
<p>Did it look  correct ?</p>



<a name="197995646"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197995646" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197995646">(May 18 2020 at 21:07)</a>:</h4>
<p>I left comments. The TL;DR is "yes but I think we might want to do it a bit differently"</p>



<a name="197995699"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197995699" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197995699">(May 18 2020 at 21:08)</a>:</h4>
<p>but I need to spend a bit of time to sketch out what I mean</p>



<a name="197995717"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197995717" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197995717">(May 18 2020 at 21:08)</a>:</h4>
<p>because it's more at "hunch" territory right now than real proposal</p>



<a name="197995769"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/197995769" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#197995769">(May 18 2020 at 21:08)</a>:</h4>
<p>that said, I think what you did matches the existing structure of the recursive solver right now, it's just that I had in mind some changes to that structure that might affect the right fix here</p>



<a name="198067670"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/198067670" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#198067670">(May 19 2020 at 13:47)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span>  That being said, should I address the feedback or wait for some further insights?</p>



<a name="198129786"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/198129786" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#198129786">(May 19 2020 at 21:33)</a>:</h4>
<p><span class="user-mention" data-user-id="283967">@Zahari Dichev</span> let me see if I can sketch out some of my ideas right now</p>



<a name="198133143"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/198133143" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#198133143">(May 19 2020 at 22:06)</a>:</h4>
<p>ok it seems clear that the first step here is probably documenting how the recursive solver works today</p>



<a name="198141622"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/198141622" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#198141622">(May 19 2020 at 23:56)</a>:</h4>
<p>started taking notes in <a href="https://hackmd.io/OocwyNPjQ6aTytdzsJz1EQ">this hackmd</a> though mostly I was bringing some of the current design back into cache</p>



<a name="198190559"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/198190559" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#198190559">(May 20 2020 at 12:28)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> This is a useful beginning. COuld not stay for the whole meeting yesterday but just looked through the hackMD doc. Is it possible that I get involved a bit more into the recursive solver stream of work? How is all that going to be organized. Are there going to be issues created for it, etc ?</p>



<a name="199202632"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199202632" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199202632">(May 29 2020 at 19:44)</a>:</h4>
<p>OK so</p>



<a name="199202659"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199202659" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199202659">(May 29 2020 at 19:44)</a>:</h4>
<p><span class="user-mention" data-user-id="283967">@Zahari Dichev</span> I've been putting some thought into this and I think that the recursive solver admits a rather simpler approach</p>



<a name="199202689"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199202689" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199202689">(May 29 2020 at 19:45)</a>:</h4>
<p>although hmm if my thesis is correct than actually I... wonder why some of the tests are failing now...</p>



<a name="199202705"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199202705" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199202705">(May 29 2020 at 19:45)</a>:</h4>
<p>And I have been struggling hard to doscover it myself...</p>



<a name="199203027"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203027" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203027">(May 29 2020 at 19:48)</a>:</h4>
<p>oh, ok , I think I know why</p>



<a name="199203119"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203119" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203119">(May 29 2020 at 19:49)</a>:</h4>
<p>so..I guess I have to finish my write-up of how the recursive solver works</p>



<a name="199203137"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203137" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203137">(May 29 2020 at 19:49)</a>:</h4>
<p>to kind of explain the proposal I have in mind :)</p>



<a name="199203152"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203152" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203152">(May 29 2020 at 19:49)</a>:</h4>
<p>but I'll try a shorter version, and maybe it helps</p>



<a name="199203174"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203174" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203174">(May 29 2020 at 19:49)</a>:</h4>
<p>the way that the recursive solver handles <strong>induction</strong> is basically by iterating</p>



<a name="199203191"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203191" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203191">(May 29 2020 at 19:49)</a>:</h4>
<p>i.e., if you are solving a goal G1</p>



<a name="199203204"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203204" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203204">(May 29 2020 at 19:49)</a>:</h4>
<p>and that requires G2 which requires G1 (say)</p>



<a name="199203366"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203366" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203366">(May 29 2020 at 19:51)</a>:</h4>
<p>we start out G1 with an interim result of "error"</p>



<a name="199203396"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203396" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203396">(May 29 2020 at 19:51)</a>:</h4>
<p>yes</p>



<a name="199203424"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203424" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203424">(May 29 2020 at 19:51)</a>:</h4>
<p>when G2 recursively reaches G1, we  will start by using that interim result, but flag (using the "minimums") that the G2 entry on the stack depends on G1</p>



<a name="199203482"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203482" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203482">(May 29 2020 at 19:52)</a>:</h4>
<p>then when G1 would be complete with some new result R, if it is not error, we re-execute G1</p>



<a name="199203488"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203488" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203488">(May 29 2020 at 19:52)</a>:</h4>
<p>and this time when the recursion occurs, we can use that new result R</p>



<a name="199203525"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203525" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203525">(May 29 2020 at 19:52)</a>:</h4>
<p>this should fairly quickly reach a fixed point, because if new results get created, then R quickly becomes "ambiguous"</p>



<a name="199203593"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203593" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203593">(May 29 2020 at 19:53)</a>:</h4>
<p>(actually I find I am a bit confused again by one of the tests and why the recursive sovler behaves as it does...)</p>



<a name="199203619"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203619" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203619">(May 29 2020 at 19:53)</a>:</h4>
<p>but anyway the basic idea that I am thinking of is that we can likely use basically the same approach for coinduction</p>



<a name="199203710"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203710" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203710">(May 29 2020 at 19:54)</a>:</h4>
<p>except that the "interim result" is not "error" but "true for everything"</p>



<a name="199203741"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203741" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203741">(May 29 2020 at 19:54)</a>:</h4>
<p>and the idea then is that the iterations are kind of "narrowing down" the cases where it's true</p>



<a name="199203766"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203766" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203766">(May 29 2020 at 19:54)</a>:</h4>
<p>instead of "expanding them", as you would for induction</p>



<a name="199203783"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203783" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203783">(May 29 2020 at 19:54)</a>:</h4>
<p>this...actually kind of makes sense if you think about what induction/co-induction are supposed to mean, now that I think about it</p>



<a name="199203842"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203842" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203842">(May 29 2020 at 19:55)</a>:</h4>
<p>so in cases like</p>
<div class="codehilite"><pre><span></span><code>C1 :- C2
C2 :- C3
C3 :- C1, C4
</code></pre></div>


<p>you would start out assuming C1 is true, but you would find it is false because C3 is false, and if you executed again, you'd reach a fixed point of false</p>



<a name="199203895"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203895" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203895">(May 29 2020 at 19:55)</a>:</h4>
<p>I'm not sure if executing again is actually needed though in that case</p>



<a name="199203933"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203933" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203933">(May 29 2020 at 19:56)</a>:</h4>
<p>because you can't get "narrower" than "never"</p>



<a name="199203974"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203974" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203974">(May 29 2020 at 19:56)</a>:</h4>
<p>but in a case like</p>
<div class="codehilite"><pre><span></span><code>C1(X) :- C2(Y), X = 22
C2(X) :- C3(X), X = 44
C3(X) :- C1(X), C2(X)
</code></pre></div>



<a name="199203985"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199203985" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199203985">(May 29 2020 at 19:56)</a>:</h4>
<p>that's more interesting</p>



<a name="199204026"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204026" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204026">(May 29 2020 at 19:56)</a>:</h4>
<p>initially you think C1 is true for all cases -- but at the end of the loop, because of <code>X = 22</code>, you find it's only true for <code>X = 22</code>, so you re-execute</p>



<a name="199204050"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204050" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204050">(May 29 2020 at 19:57)</a>:</h4>
<p>this time you'll wind up with a unification error because you'll get that <code>C3</code> is only true for <code>X = 22</code>, and that will then fail in <code>C2</code></p>



<a name="199204079"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204079" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204079">(May 29 2020 at 19:57)</a>:</h4>
<p>so in short I don't think we really need "delayed goals" or "trivial cycles" at all in this model</p>



<a name="199204083"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204083" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204083">(May 29 2020 at 19:57)</a>:</h4>
<p>it's kind of simpler</p>



<a name="199204134"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204134" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204134">(May 29 2020 at 19:57)</a>:</h4>
<p>at the cost of having to re-execute around cycles, but that's kind of the core design of the recursive solver so never mind that</p>



<a name="199204150"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204150" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204150">(May 29 2020 at 19:57)</a>:</h4>
<p>does that make sense?</p>



<a name="199204321"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204321" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204321">(May 29 2020 at 19:58)</a>:</h4>
<p>hmm will have to read over a few times to digest fully but one thing that pops out is the following. You are saying that we start out by assuming C1 to be true. How would we assume that if it s the first time we see C1. At that point we do not know there is a coinductive cycle ?</p>



<a name="199204363"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204363" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204363">(May 29 2020 at 19:59)</a>:</h4>
<p>well we know it's a coinductive goal</p>



<a name="199204413"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204413" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204413">(May 29 2020 at 19:59)</a>:</h4>
<p>the idea is that the initial value for induction is "never true" but for co-induction it's "always true"</p>



<a name="199204457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204457">(May 29 2020 at 19:59)</a>:</h4>
<p>but I have to ponder one other thing</p>



<a name="199204645"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204645" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204645">(May 29 2020 at 20:01)</a>:</h4>
<p>if you have</p>
<div class="codehilite"><pre><span></span><code>Coinductive :- Inductive
Inductive :- Coinductive
</code></pre></div>


<p>we don't want that to be accepted, I have to look back at the way some of the papers talk about it, I'm not sure if we can just always treat that as an error?</p>



<a name="199204663"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204663" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204663">(May 29 2020 at 20:01)</a>:</h4>
<p>in other words, if the stack is purely coinductive, or purely inductive,</p>



<a name="199204680"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204680" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204680">(May 29 2020 at 20:01)</a>:</h4>
<p>and you setup the initial conditions as  I said</p>



<a name="199204692"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204692" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204692">(May 29 2020 at 20:01)</a>:</h4>
<p>(and you also do the merging in the opposite direction)</p>



<a name="199204698"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204698" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204698">(May 29 2020 at 20:01)</a>:</h4>
<p>I think everything "just works"</p>



<a name="199204776"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204776" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204776">(May 29 2020 at 20:02)</a>:</h4>
<p>but I'm not sure, with mixed stacks, maybe the answer is that this is always an error (unprovable). I believe that is correct, but I have to work through some examples.</p>



<a name="199204877"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204877" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204877">(May 29 2020 at 20:03)</a>:</h4>
<p>the intuition for induction is: </p>
<ul>
<li>you need to build a proof tree with no cycles in it</li>
<li>you start with error, so that's fine, because every proof tree you sucecssfully build will be acyclic, and say that produces answer A</li>
<li>then in the next round, any proof tree you build based on A has no cycles, because it starts with A (which is acyclic) and adds whatever you added (which is finite)</li>
</ul>



<a name="199204910"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204910" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204910">(May 29 2020 at 20:03)</a>:</h4>
<p>if the process <em>terminates</em> (reaches fixed point), then you're all set</p>



<a name="199204931"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199204931" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199204931">(May 29 2020 at 20:03)</a>:</h4>
<p>in a prolog setting, it might never terminate...for us we might reach ambiguity...</p>



<a name="199205090"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205090" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205090">(May 29 2020 at 20:04)</a>:</h4>
<p>for coinduction it works a bit differently, but basically you can have cycles, as long as there are no internal errors in it, and the result will kind of work out the same way (I think)</p>



<a name="199205191"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205191" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205191">(May 29 2020 at 20:05)</a>:</h4>
<p>So <span class="user-mention" data-user-id="283967">@Zahari Dichev</span> what I might do right now</p>



<a name="199205201"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205201" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205201">(May 29 2020 at 20:05)</a>:</h4>
<p>because I'm in the mood to write some code...</p>



<a name="199205210"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205210" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205210">(May 29 2020 at 20:05)</a>:</h4>
<p>...is try to simplify and poke at the recursive solver</p>



<a name="199205220"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205220" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205220">(May 29 2020 at 20:05)</a>:</h4>
<p>I find it a bit "entangled" in its current structure, and I wanted to try and separate out the caching</p>



<a name="199205226"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205226" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205226">(May 29 2020 at 20:05)</a>:</h4>
<p>this is all very useful information</p>



<a name="199205233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205233">(May 29 2020 at 20:06)</a>:</h4>
<p>I was a bit afraid of stepping on your toes in the branch</p>



<a name="199205279"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205279" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205279">(May 29 2020 at 20:06)</a>:</h4>
<p>but now I sort of think the approach we should take would be totally different anyway</p>



<a name="199205287"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205287" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205287">(May 29 2020 at 20:06)</a>:</h4>
<p>so I'm less afraid of that :)</p>



<a name="199205379"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205379" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205379">(May 29 2020 at 20:07)</a>:</h4>
<p>yes most  likely that will be quite helpful (as opposed to stepping on my toes)</p>



<a name="199205430"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205430" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205430">(May 29 2020 at 20:07)</a>:</h4>
<p>I was wondering whether there are any conrete pieces of work I can take up on the recursive solver</p>



<a name="199205482"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205482" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205482">(May 29 2020 at 20:07)</a>:</h4>
<p>the integration with salsa and parallel querying sounds quite interesting</p>



<a name="199205488"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205488" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205488">(May 29 2020 at 20:07)</a>:</h4>
<p>what I might actually do is document it as much as refactor it</p>



<a name="199205539"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205539" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205539">(May 29 2020 at 20:08)</a>:</h4>
<p>yeah, I'd love to be working on that with you, and that's partly why I want to spend a bit of time just poking at the code</p>



<a name="199205544"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205544" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205544">(May 29 2020 at 20:08)</a>:</h4>
<p>not sure what are the next milestones for all this work</p>



<a name="199205559"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205559" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205559">(May 29 2020 at 20:08)</a>:</h4>
<p>because I can't quite "formulate the steps" in my head right now</p>



<a name="199205565"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205565" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205565">(May 29 2020 at 20:08)</a>:</h4>
<p>that sounds great</p>



<a name="199205645"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205645" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205645">(May 29 2020 at 20:09)</a>:</h4>
<p>to be painfully honest, I have spent a fair amount of time looking at the code and at times I get quite confused</p>



<a name="199205758"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205758" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205758">(May 29 2020 at 20:09)</a>:</h4>
<p>maybe the fact that I am trying to understand it by reading the SLG docs and attempting to draw a parallel does not quite help</p>



<a name="199205886"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199205886" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199205886">(May 29 2020 at 20:10)</a>:</h4>
<p>yeah it's quite different in many respects</p>



<a name="199206004"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199206004" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199206004">(May 29 2020 at 20:11)</a>:</h4>
<p>ok, I'm going to start by adding some doc comments and working on some docs then</p>



<a name="199206020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199206020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199206020">(May 29 2020 at 20:11)</a>:</h4>
<p>and maybe along the way I will see what (if any) refactorings I felt I wanted to do</p>



<a name="199218020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199218020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199218020">(May 29 2020 at 22:04)</a>:</h4>
<p>ok I started a branch here with documentation:</p>
<p><a href="https://github.com/nikomatsakis/chalk-ndm/tree/recursive-solver-document">https://github.com/nikomatsakis/chalk-ndm/tree/recursive-solver-document</a></p>



<a name="199218044"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199218044" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199218044">(May 29 2020 at 22:04)</a>:</h4>
<p>I maybe didn't get to the most interesting bits</p>



<a name="199218071"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199218071" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199218071">(May 29 2020 at 22:05)</a>:</h4>
<p>but I will :)</p>



<a name="199218082"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199218082" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199218082">(May 29 2020 at 22:05)</a>:</h4>
<p>and I think my coverage of inductive cycles more-or-less repeated some stuff that <span class="user-mention" data-user-id="131694">@scalexm</span> wrote earlier and which I realize now is probably in the chalk book somewhere else</p>



<a name="199218086"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199218086" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199218086">(May 29 2020 at 22:05)</a>:</h4>
<p>but oh well</p>



<a name="199218116"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199218116" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199218116">(May 29 2020 at 22:05)</a>:</h4>
<p>I just realized -- but I have to stop -- that I can use mermaid to draw graphs and explain some of these intutitions</p>



<a name="199218118"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199218118" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199218118">(May 29 2020 at 22:05)</a>:</h4>
<p>ooh</p>



<a name="199218126"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/199218126" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#199218126">(May 29 2020 at 22:05)</a>:</h4>
<p>ok, more later</p>



<a name="200674552"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/200674552" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#200674552">(Jun 12 2020 at 14:08)</a>:</h4>
<p>So <span class="user-mention" data-user-id="283967">@Zahari Dichev</span> I was thinking more about this and I feel like the model I semi-proposed here is the right one. I guess that per our earlier conversation I will try to leave some implementation notes today on an issue on the chalk repo?</p>



<a name="200684050"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/200684050" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zahari Dichev <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#200684050">(Jun 12 2020 at 15:22)</a>:</h4>
<p>That sounds great. I will keep an eye out for it</p>



<a name="200703786"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/200703786" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#200703786">(Jun 12 2020 at 18:04)</a>:</h4>
<p>OK, I've been writing things down, I realized in the course of doing it that this should be I think relatively easy</p>



<a name="200705993"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20in%20the%20recursive%20solver%20chalk%23399/near/200705993" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20in.20the.20recursive.20solver.20chalk.23399.html#200705993">(Jun 12 2020 at 18:20)</a>:</h4>
<p><span class="user-mention" data-user-id="283967">@Zahari Dichev</span> <a href="https://github.com/rust-lang/chalk/issues/399#issuecomment-643420016">comment</a></p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>